Step of Proof: add_functionality_wrt_le 12,41

Inference at * 1 1 
Iof proof for Lemma add functionality wrt le:



1. i1 : 
2. i2 : 
3. j2 : 
4. i2  j2
  j1:. (i1  j1 ((i1+i2 (j1+j2)) 
latex

 by (RA (IntInd 1)) 
latex


 1

 1: 1. i2 : 
 1: 2. j2 : 
 1: 3. i2  j2
 1: 4. i1 : 
 1: 5. i1 < 0
 1: 6. j1:. ((i1+1)  j1 ((i1+1+i2 (j1+j2))
 1: 7. j1 : 
 1: 8. i1  j1
 1:   (i1+i2 (j1+j2)
 2

 2: 1. i2 : 
 2: 2. j2 : 
 2: 3. i2  j2
 2: 4. j1 : 
 2: 5. 0  j1
 2:   (0+i2 (j1+j2)
 3

 3: 1. i2 : 
 3: 2. j2 : 
 3: 3. i2  j2
 3: 4. i1 : 
 3: 5. 0 < i1
 3: 6. j1:. ((i1 - 1)  j1 (((i1 - 1)+i2 (j1+j2))
 3: 7. j1 : 
 3: 8. i1  j1
 3:   (i1+i2 (j1+j2)
 .


Definitionst  T, P  Q, x:AB(x),
Lemmasle wf

origin